﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using PathSplitterUtil;
using Roslyn.Compilers.CSharp;

namespace PathSplitter
{
    public static class PathUtil
    {
        public static string GetCodeSpecializedToInput(string code, params object[] arguments)
        {
            var paths = Parser.ParsePaths<int>(code);
            var branchNamer = new IntBranchNamer();
            paths.NameBranches(branchNamer);

            var pathRecorder = new __PathRecorder();
            RosylnUtil.RunCodeOnOne(paths.ToAnnotatedCodeString(),
                                    arguments.Concat(pathRecorder.Singleton()).ToArray());

            var path = pathRecorder.Path;
            return paths.ToPathString(path.Cast<int>().ToList()).Replace("\n", "\r\n");
        }
    }

    public abstract class PathCollection<T>
    {
        protected internal static readonly IList<string> EMPTY_STRING_LIST = new string[0];

        //public abstract IEnumerable<string> Split(int maxLoopIterations);

        protected internal abstract Tuple<string, IList<string>> ToCodeStringWithAssertions(
            IList<Tuple<string, IList<string>>> childCodeStrings);

        protected internal string ToCodeString()
        {
            return ToCodeStringWithAssertions(childCodeStrings:
                Children.Select(c => Tuple.Create(c.ToCodeString(), EMPTY_STRING_LIST)).ToList()).Item1;
        }

        // Default is to just pass along that nodes that care should use annotated/per path logic.
        public virtual string ToAnnotatedCodeString()
        {
            // Annotated strings don't have assertions.
            return ToCodeStringWithAssertions(childCodeStrings:
                Children.Select(c => Tuple.Create(c.ToAnnotatedCodeString(), EMPTY_STRING_LIST)).ToList()).Item1;
        }
        internal virtual Tuple<string, IList<string>> ToPathStringWithAssertions(IList<T> path)
        {
            // TODO Note that if the path matter at this node, then the ordering of reading the path is wrong.
            //      Be careful in overrides.
            return ToCodeStringWithAssertions(childCodeStrings: Children.Select(c => c.ToPathStringWithAssertions(path)).ToList());
        }

        protected internal abstract IEnumerable<PathCollection<T>> Children { get; }

        public virtual void NameBranches(BranchNamer<T> branchNamer)
        {
            foreach (var child in Children)
            {
                child.NameBranches(branchNamer);
            }
        }

        protected internal static string GetStatementAnnotation(T branchName)
        {
            return "__pathRecorder.Add(" + ConstantUtil.ConstantToString(branchName) + ");";
        }
        protected internal static string GetExpressionAnnotation(T branchName, string expressionComputation)
        {
            return "__pathRecorder.Add(" + ConstantUtil.ConstantToString(branchName)
                + ", () => " + expressionComputation + ")";
        }
        protected internal static string ConditionToAssume(string condition)
        {
            // TODO Right form for assume?
            return "PexAssume.IsTrue(" + condition + ");";
        }
        protected internal static string FlattenAssumes(Tuple<string, IList<string>> resTup)
        {
            return (string.Join("\n", resTup.Item2.Select(ConditionToAssume)) + "\n" + resTup.Item1).Trim();
        }
    }
    public abstract class StatementPathCollection<T> : PathCollection<T>
    {
        protected internal virtual Tuple<string, IList<string>> _ToPathStringWithAssertions(IList<T> path)
        {
            return base.ToPathStringWithAssertions(path);
        }

        internal override Tuple<string, IList<string>> ToPathStringWithAssertions(IList<T> path)
        {
            var resTup = _ToPathStringWithAssertions(path);
            return Tuple.Create(FlattenAssumes(resTup), EMPTY_STRING_LIST);
        }

        public string ToPathString(IList<T> path)
        {
            //var resTup = ToPathStringWithAssertions(path);
            //return (string.Join("\n", resTup.Item2) + "\n" + resTup.Item1).Trim();
            return ToPathStringWithAssertions(path).Item1;
        }
    }
    public abstract class ConditionalStatementPathCollection<T> : StatementPathCollection<T>
    {
        protected internal abstract Tuple<string, IList<string>> GetAssertionPathString(IList<T> path);

        protected internal override Tuple<string, IList<string>> _ToPathStringWithAssertions(IList<T> path)
        {
            var assertion = GetAssertionPathString(path);
            if (path.Any())
            {
                var childSel = path.First();
                var child = Children.OfType<ConditionedStatementPathCollection<T>>()
                                    .Where(c => c.BranchName.Equals(childSel))
                                    .ToList();
                if (child.Any())
                {
                    path.Remove(childSel);
                    return Tuple.Create(child.Single().ToPathString(path),
                        assertion.Item2.Concat(assertion.Item1.Singleton()).ToIList());
                }
            }
            // Branch not taken.
            return Tuple.Create("", assertion.Item2.Concat(assertion.Item1.Singleton()).ToIList());
        }
    }
    public class ConditionalExpressionPathCollection<T> : ExpressionPathCollection<T>
    {
        private readonly ExpressionPathCollection<T> condition;
        private readonly ConditionedExpressionPathCollection<T> whenTrue;
        private readonly ConditionedExpressionPathCollection<T> whenFalse;

        public ConditionalExpressionPathCollection(ExpressionPathCollection<T> condition, ExpressionPathCollection<T> whenTrue, ExpressionPathCollection<T> whenFalse)
        {
            this.condition = condition;
            this.whenTrue = new ConditionedExpressionPathCollection<T>(whenTrue);
            this.whenFalse = new ConditionedExpressionPathCollection<T>(whenFalse);
        }
        protected internal Tuple<string, IList<string>> GetAssertionPathString(IList<T> path)
        {
            var res = condition.ToPathStringWithAssertions(path);
            if (!path[0].Equals(whenTrue.BranchName))
            {
                res = Tuple.Create("!(" + res.Item1 + ")", res.Item2);
            }
            return res;
        }

        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return new[] { condition, whenTrue, whenFalse }; }
        }

        internal override Tuple<string, IList<string>> ToPathStringWithAssertions(IList<T> path)
        {
            var assertion = GetAssertionPathString(path);
            var childSel = path.First();
            path.Remove(childSel);
            var child = Children.OfType<ConditionedExpressionPathCollection<T>>()
                                .Single(c => c.BranchName.Equals(childSel));
            var childToStr = child.ToPathStringWithAssertions(path);
            return Tuple.Create(childToStr.Item1,
                assertion.Item2.Concat(assertion.Item1.Singleton()).Concat(childToStr.Item2).ToIList());
        }

        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return Tuple.Create(childCodeStrings[0].Item1 + " ? " + childCodeStrings[1].Item1 + " : " + childCodeStrings[2].Item1,
                childCodeStrings.SelectMany(c => c.Item2).ToIList());
        }
    }
    public abstract class ConditionedStatementPathCollection<T> : StatementPathCollection<T>
    {
        public T BranchName { get; private set; }
        protected readonly StatementPathCollection<T> statement;

        public ConditionedStatementPathCollection(StatementPathCollection<T> statement)
        {
            this.statement = statement;
        }

        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return new[] { statement }; }
        }

        public override void NameBranches(BranchNamer<T> branchNamer)
        {
            BranchName = branchNamer.GetNextBranchName();
            base.NameBranches(branchNamer);
        }
    }
    public class IfBranchPathCollection<T> : ConditionedStatementPathCollection<T>
    {
        public IfBranchPathCollection(StatementPathCollection<T> statement)
            : base(statement)
        { }

        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return childCodeStrings[0];
        }

        public override string ToAnnotatedCodeString()
        {
            string annotation = GetStatementAnnotation(BranchName);
            return annotation + "\n" + base.ToAnnotatedCodeString();
        }
    }
    public abstract class ExpressionPathCollection<T> : PathCollection<T>
    {
    }
    public class ConditionedExpressionPathCollection<T> : ExpressionPathCollection<T>
    {
        public T BranchName { get; private set; }
        private readonly ExpressionPathCollection<T> expression;

        public override void NameBranches(BranchNamer<T> branchNamer)
        {
            BranchName = branchNamer.GetNextBranchName();
            base.NameBranches(branchNamer);
        }

        public ConditionedExpressionPathCollection(ExpressionPathCollection<T> expression)
        {
            this.expression = expression;
        }

        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return new[] { expression }; }
        }

        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return childCodeStrings[0];
        }

        public override string ToAnnotatedCodeString()
        {
            return GetExpressionAnnotation(BranchName, base.ToAnnotatedCodeString());
        }
    }

    public class IndentedPathCollection<T> : StatementPathCollection<T>
    {
        private readonly string header;
        private readonly string footer;
        private readonly IList<StatementPathCollection<T>> statements;

        public IndentedPathCollection(string header, string footer, IList<StatementPathCollection<T>> statements)
        {
            this.header = header;
            this.footer = footer;
            this.statements = statements;
        }
        public IndentedPathCollection(string header, string footer, StatementPathCollection<T> statement)
            : this(header: header, footer: footer, statements: statement.Singleton())
        { }
        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return statements; }
        }
        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            if (childCodeStrings.Any(c => c.Item2.Any()))
            {
                throw new Exception("Invalid childCodeStrings.");
            }
            return Tuple.Create(header + string.Join("\n\t", childCodeStrings.Select(c => c.Item1.Replace("\n", "\n\t"))).Trim() + footer, EMPTY_STRING_LIST);
        }
    }
    public class MethodPathCollection<T> : StatementPathCollection<T>
    {
        private readonly MethodDeclarationSyntax method;
        private readonly StatementPathCollection<T> body;

        private readonly string header, annotatedHeader;

        public MethodPathCollection(MethodDeclarationSyntax method, StatementPathCollection<T> body)
        {
            this.method = method;
            this.body = body;

            this.header = string.Join("", method.Modifiers) + ""
                    + method.ReturnType + "" + method.Identifier
                    + method.ParameterList.ToString().TrimEnd();
            this.annotatedHeader = string.Join("", method.Modifiers) + ""
                + method.ReturnType + "" + method.Identifier
                + method.ParameterList.OpenParenToken + string.Join(", ", method.ParameterList.Parameters) + ", __PathRecorder __pathRecorder = null"
                + method.ParameterList.CloseParenToken.ToString().TrimEnd();
        }
        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return new[] { body }; }
        }
        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            if (childCodeStrings.Any(c => c.Item2.Any()))
            {
                throw new Exception("Invalid childCodeStrings.");
            }
            return Tuple.Create(header + "\n" + childCodeStrings[0].Item1, EMPTY_STRING_LIST);
        }
        public override string ToAnnotatedCodeString()
        {
            return annotatedHeader + "\n" + body.ToAnnotatedCodeString();
        }
    }
    public class SimpleStatementPathCollection<T> : StatementPathCollection<T>
    {
        private readonly string code;

        public SimpleStatementPathCollection(string code)
        {
            this.code = code;
        }
        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return Enumerable.Empty<SimpleStatementPathCollection<T>>(); }
        }
        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return Tuple.Create(code, EMPTY_STRING_LIST);
        }
    }
    public class NormalStatementPathCollection<T> : StatementPathCollection<T>
    {
        private readonly string codeFormat;
        private readonly PathCollection<T>[] args;

        public NormalStatementPathCollection(string codeFormat, params PathCollection<T>[] args)
        {
            this.codeFormat = codeFormat;
            this.args = args;
        }
        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return args; }
        }
        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return Tuple.Create(string.Format(codeFormat, args: childCodeStrings.Select(c => c.Item1).ToArray()),
                childCodeStrings.SelectMany(c => c.Item2).ToIList());
        }
    }
    public class SimpleExpressionPathCollection<T> : ExpressionPathCollection<T>
    {
        private readonly string code;

        public SimpleExpressionPathCollection(string code)
        {
            this.code = code;
        }
        public SimpleExpressionPathCollection() : this("") { }
        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return Enumerable.Empty<SimpleStatementPathCollection<T>>(); }
        }
        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return Tuple.Create(code, EMPTY_STRING_LIST);
        }
    }
    public class NormalExpressionPathCollection<T> : ExpressionPathCollection<T>
    {
        private readonly string codeFormat;
        private readonly ExpressionPathCollection<T>[] args;

        public NormalExpressionPathCollection(string codeFormat, params ExpressionPathCollection<T>[] args)
        {
            this.codeFormat = codeFormat;
            this.args = args;
        }
        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return args; }
        }
        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return Tuple.Create(string.Format(codeFormat, args: childCodeStrings.Select(c => c.Item1).ToArray()),
                childCodeStrings.SelectMany(c => c.Item2).ToIList());
        }
    }

    public class IfPathCollection<T> : ConditionalStatementPathCollection<T>
    {
        private readonly ExpressionPathCollection<T> condition;
        private readonly ConditionedStatementPathCollection<T> ifBlock, elseBlock;

        public IfPathCollection(ExpressionPathCollection<T> condition,
            StatementPathCollection<T> ifBlock,
            StatementPathCollection<T> elseBlock)
        {
            this.condition = condition;
            this.ifBlock = new IfBranchPathCollection<T>(ifBlock);
            this.elseBlock = elseBlock == null ? null : new IfBranchPathCollection<T>(elseBlock);
        }
        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get
            {
                yield return condition;
                yield return ifBlock;
                if (elseBlock != null)
                    yield return elseBlock;
            }
        }
        protected internal override Tuple<string, IList<string>> GetAssertionPathString(IList<T> path)
        {
            var res = condition.ToPathStringWithAssertions(path);
            if (!path.Any() || !ifBlock.BranchName.Equals(path.First()))
            {
                res = Tuple.Create("!(" + res.Item1 + ")", res.Item2);
            }
            return res;
        }
        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return Tuple.Create("if(" + childCodeStrings[0].Item1 + ") {\n\t"
                + childCodeStrings[1].Item1
                + (elseBlock != null ? "\n} else {\n\t" + childCodeStrings[2].Item1 + "\n}" : "\n}"), childCodeStrings[0].Item2);
        }
    }

    public class SwitchSectionPathCollection<T> : ConditionedStatementPathCollection<T>
    {
        private readonly IList<string> labels;

        public SwitchSectionPathCollection(IList<string> labels, IndentedPathCollection<T> statements)
            : base(statements)
        {
            this.labels = labels;
        }

        internal string GetCaseEqualsString(string expr)
        {
            if (labels.Any(l => l == null))
            {
                return "true";
            }
            else
            {
                return string.Join(" || ", labels.Select(l => "(" + l + " == " + expr + ")"));
            }
        }

        protected internal Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings, bool annotate)
        {
            if (childCodeStrings[0].Item2.Any())
            {
                throw new Exception("Assertions must already be flattened into case body.");
            }
            return Tuple.Create(string.Join("\n", labels.Select(l => l == null ? "default:" : "case " + l + ":"))
                + "\n\t" + (annotate ? GetStatementAnnotation(this.BranchName) + "\n\t" : "") + childCodeStrings[0].Item1, EMPTY_STRING_LIST);
        }
        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return this.ToCodeStringWithAssertions(childCodeStrings, annotate: false);
        }

        public override string ToAnnotatedCodeString()
        {
            // Annotated strings don't have assertions.
            return ToCodeStringWithAssertions(childCodeStrings:
                    Children.Select(c => Tuple.Create(c.ToAnnotatedCodeString(), EMPTY_STRING_LIST)).ToList(),
                annotate: true).Item1;
        }

        internal override Tuple<string, IList<string>> ToPathStringWithAssertions(IList<T> path)
        {
            return statement.ToPathStringWithAssertions(path);
        }
    }
    public class SwitchPathCollection<T> : ConditionalStatementPathCollection<T>
    {
        private ExpressionPathCollection<T> expressionPaths;
        private List<SwitchSectionPathCollection<T>> sections;

        public SwitchPathCollection(ExpressionPathCollection<T> expressionPaths, List<SwitchSectionPathCollection<T>> sections)
        {
            this.expressionPaths = expressionPaths;
            this.sections = sections;
        }

        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return expressionPaths.Cons<PathCollection<T>>(sections); }
        }

        protected internal override Tuple<string, IList<string>> GetAssertionPathString(IList<T> path)
        {
            var res = expressionPaths.ToPathStringWithAssertions(path);
            return Tuple.Create(
                sections.Single(s => s.BranchName.Equals(path[0]))
                                .GetCaseEqualsString(res.Item1),
                res.Item2);
        }

        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            return Tuple.Create("switch(" + childCodeStrings[0].Item1 + ") {\n"
                + string.Join("\n", childCodeStrings.Skip(1).Select(c => c.Item1))
                + "\n}", childCodeStrings.SelectMany(l => l.Item2).ToIList());
            throw new NotImplementedException();
        }
    }

    public abstract class LoopPathCollection<T> : StatementPathCollection<T>
    {
        public T BranchName { get; private set; }
        protected internal abstract StatementPathCollection<T> LoopBody { get; }

        public override void NameBranches(BranchNamer<T> branchNamer)
        {
            BranchName = branchNamer.GetNextBranchName();
            base.NameBranches(branchNamer);
        }

        protected internal override Tuple<string, IList<string>> ToCodeStringWithAssertions(IList<Tuple<string, IList<string>>> childCodeStrings)
        {
            throw new Exception("ToCodeStringWithAssertions should not be needed for LoopPathCollections.");
        }

        public override string ToAnnotatedCodeString()
        {
            return ToCodeString(annotated: true);
        }
        
        private string ToCodeString(bool annotated)
        {
            return GetHeaderString(annotated)
                + GetBodyString(annotated)
                + GetFooterString(annotated);
        }

        private string GetBodyString(bool annotated)
        {
            if (annotated)
            {
                string annotation = GetStatementAnnotation(BranchName);
                return "{\n\t" + annotation + "\n\t" + LoopBody.ToAnnotatedCodeString() + "\n}";
            }
            else
            {
                return LoopBody.ToCodeString();
            }
        }

        internal override Tuple<string, IList<string>> ToPathStringWithAssertions(IList<T> path)
        {
            string res = GetHeaderForFirstIteration(path) + "\n";
            var loopCondition = GetLoopConditionString(path);
            while (path.Any() && BranchName.Equals(path.First()))
            {
                path.RemoveAt(0);
                res += FlattenAssumes(Tuple.Create(ConditionToAssume(loopCondition.Item1), loopCondition.Item2))
                    + "\n" + GetBodyPathString(path) + "\n";
                loopCondition = GetLoopConditionString(path);
            }
            res += FlattenAssumes(Tuple.Create(ConditionToAssume("!(" + loopCondition.Item1 + ")"), loopCondition.Item2));
            return Tuple.Create(res.Trim(), EMPTY_STRING_LIST);
        }

        protected internal abstract string GetHeaderString(bool annotated);
        protected internal virtual string GetFooterString(bool annotated)
        {
            return "";
        }

        protected internal abstract Tuple<string, IList<string>> GetLoopConditionString(IList<T> path);
        protected internal abstract string GetBodyPathString(IList<T> path);
        protected internal abstract string GetHeaderForFirstIteration(IList<T> path);
    }

    public abstract class WhileStyleLoopPathCollection<T> : LoopPathCollection<T>
    {
        private ExpressionPathCollection<T> loopCondition;
        private StatementPathCollection<T> loopBody;

        protected internal ExpressionPathCollection<T> LoopCondition { get { return loopCondition; } }
        protected internal override StatementPathCollection<T> LoopBody { get { return loopBody; } }

        public WhileStyleLoopPathCollection(ExpressionPathCollection<T> loopCondition, StatementPathCollection<T> loopBody)
        {
            this.loopCondition = loopCondition;
            this.loopBody = loopBody;
        }

        protected internal override Tuple<string, IList<string>> GetLoopConditionString(IList<T> path)
        {
            return loopCondition.ToPathStringWithAssertions(path);
        }

        protected internal override string GetBodyPathString(IList<T> path)
        {
            return loopBody.ToPathString(path);
        }
    }

    public class ForPathCollection<T> : WhileStyleLoopPathCollection<T>
    {
        private ExpressionPathCollection<T> loopDecls;
        private List<ExpressionPathCollection<T>> loopIncrementors;

        public ForPathCollection(StatementPathCollection<T> loopBody, ExpressionPathCollection<T> loopDecls, ExpressionPathCollection<T> loopCondition, List<ExpressionPathCollection<T>> loopIncrementors)
            : base(loopBody: loopBody, loopCondition: loopCondition)
        {
            this.loopDecls = loopDecls ?? new SimpleExpressionPathCollection<T>();
            this.loopIncrementors = loopIncrementors;
        }

        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get
            {
                if (loopDecls != null)
                {
                    yield return loopDecls;
                }
                yield return LoopCondition;
                yield return LoopBody;
                foreach (var inc in loopIncrementors)
                {
                    yield return inc;
                }
            }
        }

        protected internal override string GetHeaderString(bool annotated)
        {
            return "for("
                + (annotated ? loopDecls.ToAnnotatedCodeString() : loopDecls.ToCodeString())
                + ";"
                + (annotated ? LoopCondition.ToAnnotatedCodeString() : loopDecls.ToCodeString())
                + ";"
                + string.Join(", ", loopIncrementors.Select(i => annotated ? i.ToAnnotatedCodeString() : i.ToCodeString()))
                + ")";
        }

        protected internal override string GetHeaderForFirstIteration(IList<T> path)
        {
            return FlattenAssumes(loopDecls.ToPathStringWithAssertions(path))
                + (loopDecls is SimpleExpressionPathCollection<T> ? "" : ";");
        }

        protected internal override string GetBodyPathString(IList<T> path)
        {
            string res = base.GetBodyPathString(path);
            foreach (var inc in loopIncrementors)
            {
                res += "\n" + FlattenAssumes(inc.ToPathStringWithAssertions(path)) + ";";
            }
            return res;
        }
    }
    public class WhilePathCollection<T> : WhileStyleLoopPathCollection<T>
    {
        public WhilePathCollection(ExpressionPathCollection<T> loopCondition, StatementPathCollection<T> loopBody)
            : base(loopBody: loopBody, loopCondition: loopCondition)
        { }

        protected internal override string GetHeaderString(bool annotated)
        {
            return "while(" + (annotated ? LoopCondition.ToAnnotatedCodeString() : LoopCondition.ToCodeString()) + ")";
        }

        protected internal override string GetHeaderForFirstIteration(IList<T> path)
        {
            return "";
        }

        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return new PathCollection<T>[] { LoopCondition, LoopBody }; }
        }
    }

    public class DoWhilePathCollection<T> : WhileStyleLoopPathCollection<T>
    {
        public DoWhilePathCollection(ExpressionPathCollection<T> loopCondition, StatementPathCollection<T> loopBody)
            : base(loopBody: loopBody, loopCondition: loopCondition)
        { }

        protected internal override string GetHeaderString(bool annotated)
        {
            return "do";
        }

        protected internal override string GetFooterString(bool annotated)
        {
            return "while(" + (annotated ? LoopCondition.ToAnnotatedCodeString() : LoopCondition.ToCodeString()) + ");";
        }

        protected internal override string GetHeaderForFirstIteration(IList<T> path)
        {
            if (!path[0].Equals(BranchName))
            {
                throw new Exception();
            }
            path.RemoveAt(0);
            return GetBodyPathString(path);
        }

        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return new PathCollection<T>[] { LoopBody, LoopCondition }; }
        }
    }

    public class ForEachPathCollection<T> : LoopPathCollection<T>
    {
        private ExpressionPathCollection<T> expression;
        private StatementPathCollection<T> loopBody;
        private string typeName;
        private string loopVar;
        private string enumeratorName;

        public ForEachPathCollection(ExpressionPathCollection<T> expression, StatementPathCollection<T> loopBody, string typeName, string loopVar, string enumeratorName)
        {
            this.expression = expression;
            this.loopBody = loopBody;
            this.typeName = typeName;
            this.loopVar = loopVar;
            this.enumeratorName = enumeratorName;
        }

        protected internal override StatementPathCollection<T> LoopBody
        {
            get { return loopBody; }
        }

        protected internal override string GetHeaderString(bool annotated)
        {
            var exprStr = annotated ? expression.ToAnnotatedCodeString() : expression.ToCodeString();
            return "foreach(" + typeName + " " + loopVar + " in " + exprStr + ")";
        }

        protected internal override Tuple<string, IList<string>> GetLoopConditionString(IList<T> path)
        {
            return Tuple.Create(enumeratorName + ".MoveNext()", EMPTY_STRING_LIST);
        }

        protected internal override string GetBodyPathString(IList<T> path)
        {
            return loopVar + " = " + enumeratorName + ".Current;\n"
                    + loopBody.ToPathString(path) + "\n";
        }

        protected internal override string GetHeaderForFirstIteration(IList<T> path)
        {
            var tup = expression.ToPathStringWithAssertions(path);
            var assumes = tup.Item2;
            var enumerable = tup.Item1;
            return typeName + " " + loopVar + ";\n"
                    + FlattenAssumes(Tuple.Create("var " + enumeratorName
                    + " = (" + enumerable + ").AsEnumerable().GetEnumerator();",
                assumes));
        }

        protected internal override IEnumerable<PathCollection<T>> Children
        {
            get { return new PathCollection<T>[] { expression, loopBody }; }
        }
    }
}
